\begin{tabbing}
$\forall$$r$:Rng, $a$, $b$:$\mathbb{Z}$.
\\[0ex]($a$ $\leq$ $b$)
\\[0ex]$\Rightarrow$ \=($\forall$$E$, $F$:(\{$a$..$b$$^{-}$\}$\rightarrow\mid$$r$$\mid$).\+
\\[0ex]($\Sigma$\=($r$) $a$ $\leq$ $i$ $<$ $b$\+
\\[0ex]$E$($i$) +$r$ $F$($i$))
\-\\[0ex]=
\\[0ex](($\Sigma$($r$) $a$ $\leq$ $i$ $<$ $b$. $E$($i$)) +$r$ ($\Sigma$($r$) $a$ $\leq$ $i$ $<$ $b$. $F$($i$)))
\\[0ex]$\in$ $\mid$$r$$\mid$)
\-
\end{tabbing}